A1, A2:Type, l1, l2:IdLnk, tg1, tg2:Id, ds1, ds2:x:Id fp Type,
conds1:k:Knd fp V:Type  (State(ds1)V(A1 + Top)),
conds2:k:Knd fp V:Type  (State(ds2)V(A2 + Top)).
(k:Knd. (k  dom(conds1))  (hasloc(k;source(l1))))
 (k:Knd. (k  dom(conds2))  (hasloc(k;source(l2))))
 ((source(l1) = source(l2)  Id))
 ((rcv(l2,tg2)  fpf-domain(conds1))  (A2 r (conds1(rcv(l2,tg2)).1)))
 ((rcv(l1,tg1)  fpf-domain(conds2))  (A1 r (conds2(rcv(l1,tg1)).1)))
 triggersGlue(A1; l1; tg1; ds1; conds1) || triggersGlue(A2; l2; tg2; ds2; conds2) 

latex

Definitions

Top, left + right, x:AB(x), x:A. B(x), State(ds), Type, x:A  B(x), x.A(x), x. t(x), a:A fp B(a), P  Q, IdLnk, Id, source(l), hasloc(k;i), b, KindDeq, x  dom(f), s = t, , A, rcv(l,tg), f(x), t.1, (x  l), triggersGlue(A; l; tg; ds; conds), A || B, fpf-domain(f), Knd, type List, t  T, R-icompat(A;B), P & Q, Void, False, Atom$n, if b then t else f fi , a < b, x:A. B(x), R-has-loc(R;i), P  Q, P  Q, es realizer ind Rplus compseq tag def, Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), (L), Rnone(), Rsframe(lnk;tag;L), {x:A| B(x)} , trigger-send(A;ds;x;cond;l;tg), xL.R(x), left  right, es realizer ind Rsframe compseq tag def, True, b, , a = b, Unit, Rsends-T(x1), Rsends-dt(x1), Rsends-l(x1), Rsends-knd(x1), Rsends?(x1), Reffect-T(x1), Reffect-knd(x1), Reffect?(x1), R-interface-compat(A;B), R-loc(R), #$n, ||as||, A  B, , , l[i], A c B, EqDecider(T), xL. P(x), es realizer ind Rsends compseq tag def, es realizer ind Rnone compseq tag def, Rinterface(A), x : v, tag(k), IdDeq, f  g, <a, b>, [], [car / cdr], Rsends(ds;knd;T;l;dt;g), ff, tt, let x,y = A in B(x;y), if a=1 b then x else y, case b of inl(x) => s(x) | inr(y) => t(y), let x = a in b(x), lnk(k), isrcv(k), f(x)?z, isrcvl(l;k), T, destination(l), {T}, SQType(T), s ~ t, x:A.B(x), f(a)

Lemmas

Rnone-icompat, IdLnk sq, Knd sq, isrcv-implies, fpf-single-dom, id-deq wf, fpf-single wf, tagof wf, assert-hasloc, Id sq, ldst wf, squash wf, isrcvl wf, assert-isrcvl, false wf, isrcv wf, lnk wf, R-icompat-Rplus2, and functionality wrt iff, l all wf2, true wf, R-interface-compat wf, btrue wf, bfalse wf, R-icompat wf, Rall-icompat, Rplus wf, Rall wf, R-icompat symmetry, Rinterface-icompat, Rnone wf, R-icompat-Rall, nat wf, length wf1, select wf, trigger-send wf, Rsframe wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, member-fpf-dom, R-has-loc wf, triggersGlue-has-loc, R-compat-disjoint, triggersGlue wf, l member wf, rcv wf, pi1 wf, fpf-ap wf, not wf, fpf-dom wf, Kind-deq wf, assert wf, hasloc wf, lsrc wf, Knd wf, fpf wf, Id wf, IdLnk wf, fpf-domain wf, fpf-trivial-subtype-top, decl-state wf, top wf